#include "../../../../../Sarlab/trunk/padata/third/yices/yicesl_c.h"
#include <stdio.h>
void display(yicesl_context ctx) {
      if (yicesl_inconsistent(ctx)) 
              printf("unsatisfiable\n"); 
        else
                printf("satisfiable\n");
}

int main3() {
    yicesl_context ctx = yicesl_mk_context();
    yicesl_set_output_file(".yices-output");
    yicesl_read(ctx, "(define x::int)");
    yicesl_read(ctx, "(define y::int)");
    yicesl_read(ctx, "(assert (= (+ x y) 0))");
    yicesl_read(ctx, "(assert (>= y 0))");
    display(ctx);
    yicesl_read(ctx, "(push)");
    yicesl_read(ctx, "(assert (>= x 1))");
    display(ctx);
    yicesl_read(ctx, "(pop)");
    yicesl_read(ctx, "(assert (>= x 0))");
    display(ctx);
    yicesl_read(ctx, "(set-evidence! true)");
    yicesl_read(ctx, "(check)");
    yicesl_del_context(ctx);
    return 0;
}

